Of wlp and CSP

摘要

We extend Morgan's well-known derivation of the Failures-Divergences semantics of an action system endowed with a wp sequential semantics, by showing how various other CSP semantics can be extracted from an action system endowed with an appropriate sequential semantics. In doing so we expose the close but hitherto largely overlooked correspondence between the various CSP semantic models and their sequential correctness counterparts.